Add option to generate function body to goto-instrument #1889

hannes-steffenhagen-diffblue · 2018-02-27T17:10:32Z

This adds the commandline parameters --replace-function-body and --replace-function-body-options. The first gets a regex that defines a set of functions whose body should be replaced; Whereas the latter specifies what kind of body should be generated. The options here are:

nondet-return same as havoc without further options
assert-false generate a single assert(false); in the body.
assume-false generate a single assume(false); in the body (this has a similar effect to --undefined-function-is-assume-false)
havoc[,params][,globals:<regex>] which generates a return nondet for non-void functions and assigns nondet to the targets of pointers to non-const if params is set and assignments of nondet to non-const globals matching the regex if it is set.

Other than that, I'm looking for comments on the command line parameters (I've put the function "goals" and the options for the body replacement in separate options for now, but it feels a bit wordy).

tautschnig · 2018-02-27T18:51:22Z

May I start with a few questions:

I believe the existing remove-function-body should either be removed and instead yield a meaningful error message or be made to redirect to replace-function-body+havoc.
What is the relationship to Block function command line option #1566?
What is the relationship to Havoc non det functions #1585?

hannes-steffenhagen-diffblue · 2018-02-28T10:55:27Z

@tautschnig

Can you elaborate? One ends with the function having no body, the other ends with the function having a body with (possibly) a return nondet; which are "distinguishable" states. Are you saying these should be the same somehow?
Block function command line option #1566 Replaces calls to a certain function by assume_false; This behaves similarly to undefined-function-is-assume false but with a certain target function rather than with all undefined functions. This somewhat overlaps with --replace -function-body-options assume-false: The net effect for a "full" goto binary is roughly the same I think, but there are still some differences (for example, you can use replace-function-body on just the goto binary containing the function to replace and then link, whereas you'd need to use make-function-assume-false on all goto-binaries containing the function calls or call it after linking; It also needs to look at all instructions whereas replace-function-body just needs to iterate over the functions, so there might be a slight performance advantage there, though I don't expect it to be particularly large).
Havoc non det functions #1585 behaves similarly to --replace-function-body-options havoc,params; The difference being that this PR does the "nondetting" of parameters by actually replacing the function body, whereas in the other PR this is done during abstract interpretation (I'm told actually symex) (and thus needs to be implemented separately for each domain). In that PR @peterschrammel suggested doing this through a goto transformation which this PR is attempting to do. Currently it's only doing the simplest approximation of this, which is just directly assigning nondet to the pointer targets; Some other things that are "thinkable" are recursively assigning nondet values to non-null pointers, struct members and array elements (for constant size arrays), but I wanted to know what others think about this before going too crazy on it.

hannes-steffenhagen-diffblue

Add a test for function name regex

Add a test for replace-function-body-options skip

Add an option for assert-false-then-assume-false

hannes-steffenhagen-diffblue · 2018-03-08T16:19:12Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1522,8 +1533,13 @@ void goto_instrument_parse_optionst::help()
    " --remove-pointers            converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
    " --splice-call caller,callee  prepends a call to callee in the body of caller\n"  // NOLINT(*)
    // NOLINTNEXTLINE(whitespace/line_length)
-    " --undefined-function-is-assume-false\n" // NOLINTNEXTLINE(whitespace/line_length)
-    "                              convert each call to an undefined function to assume(false)\n"


Removed text that should still be there

hannes-steffenhagen-diffblue · 2018-03-08T16:20:00Z

src/goto-instrument/replace_function_bodies.cpp

+  {
+    function.body.clear();
+    generate_parameter_names(function, symbol_table, function_name);
+    replace_function_body_impl(function, symbol_table, function_name);


Should be "generate_function_body", because the body has already been removed here

hannes-steffenhagen-diffblue · 2018-03-08T16:20:52Z

src/goto-instrument/replace_function_bodies.cpp

+    goto_functiont &function,
+    symbol_tablet &symbol_table,
+    irep_idt function_name) override
+  {


Put a skip instruction here or rename this to empty

hannes-steffenhagen-diffblue · 2018-03-08T16:21:18Z

src/goto-instrument/replace_function_bodies.cpp

+public:
+  havoc_replace_function_bodiest(
+    std::vector<irep_idt> globals_to_havoc,
+    bool havoc_parameters)


Use regex for parameter instead of all-in boolean parameter

hannes-steffenhagen-diffblue · 2018-03-08T16:22:53Z

src/goto-instrument/replace_function_bodies.cpp

+  bool havoc_parameters;
+};
+
+std::unique_ptr<replace_function_bodiest> parse_replace_function_body_options(


Rename this to "factory..."

hannes-steffenhagen-diffblue · 2018-03-08T16:23:40Z

src/goto-instrument/replace_function_bodies.cpp

+  const std::regex &functions_regex,
+  const std::string &replace_options)
+{
+  messaget messages;


pass this as parameter instead

hannes-steffenhagen-diffblue · 2018-03-08T16:24:32Z

src/goto-instrument/replace_function_bodies.h

+
+Module: Replace bodies of goto functions
+
+Author: DiffBlue Limited. All rights reserved.


martin-cs · 2018-03-08T16:31:15Z

For the record, the comments above are a composite of mine and @chrisr-diffblue 's reviews of this done sat with @hannes-steffenhagen-diffblue . Beyond these we are happy to merge this.

martin-cs · 2018-03-08T16:37:54Z

There are questions of condensing other options and other functionality. This patch is the first step of a not-as-covert-as-it-was-before-I-started-writing-this attempt to remove the special case code for functions without bodies from the various analyses. In line with this I think we should also:

Redirect --remove-function-body as @tautschnig suggests.
Redirect (and update the description of) --undefined-functions-are-assume-false so that it instead generates function bodies with assume-false in them.

@tautschnig @peterschrammel opinions?

Also @polgreen does the functionality in this PR cover the use cases you had for #1566 and #1585 ?

martin-cs · 2018-03-08T16:41:29Z

@hannes-steffenhagen-diffblue : one thing I forgot when we were writing up the review, can we have an option --generate-function-bodies which is --replace-function-body for all functions which don't have a body at the moment.

hannes-steffenhagen-diffblue · 2018-03-13T13:30:03Z

@martin-cs I think that's all the comments addressed, except for the option merging thing (maybe separate PR?). Mind taking another look?

thk123

Not reviewed tests

thk123 · 2018-03-15T11:01:33Z

regression/goto-instrument/generate-function-body/test.desc

+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[main.assertion.1\] assertion does_not_get_reached: SUCCESS$
+^\[should_be_generated.assertion.1\] assertion FALSE: FAILURE$


Missing new line

thk123 · 2018-03-15T11:03:18Z

src/goto-instrument/goto_instrument_parse_options.cpp

+    std::regex function_regex = std::regex(
+      only_generate ? cmdline.get_value("generate-function-body")
+                    : cmdline.get_value("replace-function-body"));
+    status() << "Replacing function bodies" << eom;


Should this method say "Generating function bodies" if cmdline.get_value("generate-function-body")

thk123 · 2018-03-15T11:04:19Z

src/goto-instrument/goto_instrument_parse_options.h

@@ -86,7 +86,11 @@ Author: Daniel Kroening, [email protected]
  "(undefined-function-is-assume-false)" \
  "(remove-function-body):"\
  "(splice-call):" \
-  OPT_REMOVE_CALLS_NO_BODY
+  OPT_REMOVE_CALLS_NO_BODY \
+  "(replace-function-body):" \


But these options and their documentation in to replace_function_bodies.h to make it easier for it to be reused in different front ends.

As a define like some of the other options?

thk123 · 2018-03-15T11:06:03Z

src/goto-instrument/goto_instrument_parse_options.cpp

+    cmdline.isset("replace-function-body") ||
+    cmdline.isset("generate-function-body"))
+  {
+    if(


I have a mild preference to remove this code from here and put into the constructor of replace_function_bodiest so that the logic of how these parameters are handled is separated from the specific binary being used.

I was actually the opposite; I had considered doing the parsing of the arguments outside of replace_function_bodiest entirely to avoid passing more "meaningful" strings around than we really have to

My reason was that if someone wishes to re-use this they must copy/paste the interface to provide a consistent experience for the user. Rather than passing raw strings, what if you pass the whole cmdlinet into it? So it is clear they aren't meaningful strings but really the user input.

The down side to my suggestion is becomes a class that is both responsible for generating functions and parsing command line args. Perhaps it would be better to have a third place that takes a cmdline and returns a replace_goto_functionst, but OK with leaving that to the first person who wishes to re-use this code.

I'd like to support @thk123's position: In order to achieve what #1949 says, we will need this in all front-ends. So we really don't want to reimplement the command-line parsing multiple times. In my opinion, the last suggestion to have "a third place that takes a cmdline and returns..." is the best approach.

Pushing the only_generate and function_regex logic into a reusable helper in replace_function_bodies would be preferable.

thk123 · 2018-03-15T11:08:24Z

src/goto-instrument/replace_function_bodies.cpp

+  throw replace_function_body_parse_error("Can't parse \"", options, "\"");
+}
+
+void replace_function_bodies(


As the interface to this whole functionality, could you add documentation here.

thk123 · 2018-03-15T11:18:18Z

src/goto-instrument/replace_function_bodies.cpp

+  }
+};
+
+class assume_false_replace_function_bodiest : public replace_function_bodiest


Consider documenting each of these classes with:
a) the arugments needed to use them
b) a C style code block of what will be produced

You might also consider writing some really simple unit tests for each of these classes to verify the program produced.

thk123 · 2018-03-15T11:24:18Z

src/goto-instrument/replace_function_bodies.cpp

+    {
+      if(
+        parameter.type().id() == ID_pointer &&
+        !parameter.type().subtype().get_bool(ID_C_constant) &&


Not sure, but perhaps this is the same condition as is_constant_or_has_constant_components (e.g. is pointer to a pointer to a constant?)

I'm not sure; Actually it's also possible that this is the better version; i.e. you can absolutely assign a pointer-to-pointer-to-constant. Then again, structs with constant members usually aren't assignable so I'm not 100% clear on what the correct way to do this here is

Consider writing unit tests to figure out - I think it should be clear what is "correct" when you do this

thk123 · 2018-03-15T11:25:31Z

src/goto-instrument/replace_function_bodies.cpp

+};
+
+static std::vector<std::string>
+tokenize(const std::string &base, char separator)


Document? Also surely this code exists somewhere already? Is it not split_string in string_utils.cpp?

thk123 · 2018-03-15T11:26:37Z

src/goto-instrument/replace_function_bodies.cpp

+}
+
+static void write_to_stream(std::ostream &out)
+{


This is just to have a convenient method to assemble a string... Didn't end up actually needed it here so I'm removing it, but I figure something along those lines might be useful for string-utils?

Maybe? I'll reserve judgement until I see a PR with it being used 😛

thk123 · 2018-03-15T11:29:08Z

src/goto-instrument/replace_function_bodies.cpp

+      const std::vector<std::string> key_value_pair = tokenize(tokens[i], ':');
+      if(key_value_pair.size() != 2)
+      {
+        throw replace_function_body_parse_error(


Avoid introducing throw std::string type statements, consider having a replace_function_body_exceptiont for this

Should it be a child of std::runtime_error? If yes, should the message include __FILE__ and __LINE__?

They both sound like sensible suggestions to me.

hannes-steffenhagen-diffblue · 2018-03-16T14:43:50Z

@thk123 I think I've addressed most of your comments, mind having another look?

thk123 · 2018-03-19T10:54:57Z

src/goto-instrument/replace_function_bodies.h

+#include <util/message.h>
+
+/// Replace function bodies with some default behavior
+/// Can generate the following types of function bodies:


Explain the lhs of this list is the command line argument

thk123 · 2018-03-19T10:55:40Z

src/goto-instrument/replace_function_bodies.h

+///   return nondet_int();
+/// }
+///
+/// nondet-return return nondet for non-void functions


Nit: nondet-return: return nondet for non-void functions (missing colon separating command line from result)

thk123 · 2018-03-19T10:56:37Z

src/goto-instrument/replace_function_bodies.h

+/// @param functions_regex Replace bodies of functions whose names matches regex
+/// @param only_generate When true, skip functions that already have a body
+/// @param replace_options Options string indicating what body to generate
+/// @param messages Destination for status/warning messages


\param also this documentation should go in the cpp next to the implementation rather than the header (as per coding guidelines)

I also think it would be more useful to split each up to go with the corresponding class but that might just be personal preference

thk123 · 2018-03-19T11:00:46Z

src/goto-instrument/replace_function_bodies.cpp

+        new_param_sym.type = parameter.type();
+        new_param_sym.base_name = param_base_name;
+        new_param_sym.mode = ID_C;
+        auto &function_symbol = symbol_table.lookup_ref(function_name);


I think it is clearer if you make the const here explicit.

thk123 · 2018-03-19T11:03:32Z

src/goto-instrument/replace_function_bodies.cpp

+    {
+      if(
+        parameter.type().id() == ID_pointer &&
+        !parameter.type().subtype().get_bool(ID_C_constant) &&


Consider writing unit tests to figure out - I think it should be clear what is "correct" when you do this

hannes-steffenhagen-diffblue · 2018-03-29T13:48:23Z

@peterschrammel @thk123 @tautschnig @martin-cs

Can you please check whether or not you feel that your comments have been addressed?

tautschnig

Thanks a lot for the updates; still a few smaller issues, but mainly I'm wondering about the set options/the discussion around that, if it has taken place.

tautschnig · 2018-03-29T13:53:34Z

src/goto-programs/replace_function_bodies.cpp

+
+Module: Replace bodies of goto functions
+
+Author: DiffBlue Limited.


tautschnig · 2018-03-29T13:54:36Z

src/goto-programs/replace_function_bodies.cpp

+    };
+    auto assert_instruction = add_instruction();
+    assert_instruction->make_assertion(false_exprt());
+    // assert_instruction->code = code_assertt(false_exprt());


No need for this commented-out code, please remove.

tautschnig · 2018-03-29T13:57:03Z

src/goto-programs/replace_function_bodies.cpp

+  {
+    throw replace_function_bodies_errort(
+      "can only use one of --replace-function-body "
+      "or --generate-function-body");


@hannes-steffenhagen-diffblue @peterschrammel - did you discuss this? What was the conclusion, or maybe why was my proposal not acceptable?

@tautschnig Nobody else said anything about this. It's possible that they missed it. I wouldn't mind implementing it that way, but it wasn't obviously better than the current behaviour from my perspective, I'd prefer at least one other person saying they think it's the better way to do it before going ahead with changing the options at this point.

Poking @martin-cs @chrisr-diffblue with the hope that more people might chime in. Everyone: see the discussion in #1889 (comment) for context.

I've left a comment in that discussion thread - but bottom line is that I agree with @tautschnig's proposal.

tautschnig · 2018-03-29T13:57:51Z

src/goto-programs/replace_function_bodies.cpp

+/// A list of currently accepted command line arguments
+/// + the type of bodies generated by them
+///
+/// assert-false: { __CPROVER_assert(false); }


__CPROVER_assert takes a second argument.

Ah. I should probably just use assert here, the __CPROVER doesn't really add to the legibility of the example

tautschnig · 2018-03-29T13:58:17Z

src/goto-programs/replace_function_bodies.h

+
+Module: Replace bodies of goto functions
+
+Author: DiffBlue Ltd.


tautschnig · 2018-03-29T13:58:45Z

src/goto-programs/replace_function_bodies.h

+#include <util/std_types.h>
+#include <util/message.h>
+#include <goto-programs/goto_model.h>
+#include <util/cmdline.h>


Please try to sort internal includes lexicographically.

thk123

New changes seem fine but I think a bit more context on the slightly wrong test would be in order.

thk123 · 2018-04-03T09:42:33Z

regression/goto-instrument/replace-function-body-struct-with-const-member/main.c

+  havoc_struct(&paramStruct);
+  assert(globalStruct.non_const == 10);
+  assert(globalStruct.is_const == 20);
+  assert(paramStruct.non_const == 11);


Why is this not been havoced? (A good technique for trying to verify these tests is to try and write bodies that violate this asserts, for example for this can you not do:

(*WithConstMember).non_const = 20;

thk123 · 2018-04-03T09:44:52Z

src/goto-programs/replace_function_bodies.h

+      const irep_idt &function_name);
+
+private:
+  /// Generate parameter names for unnamed parameters.


Comments should go with the implementation

thk123 · 2018-04-03T09:45:12Z

src/goto-programs/replace_function_bodies.cpp

@@ -0,0 +1,410 @@
+/*******************************************************************\


I'm assuming this is a move of the original?

thk123 · 2018-04-03T09:51:58Z

regression/goto-instrument/replace-function-body-struct-with-const-member/main.c

+{
+  struct WithConstMember paramStruct = {11, 21};
+  havoc_struct(&paramStruct);
+  assert(globalStruct.non_const == 10);


In fact - since you are also havocing globals, shouldn't this assert fail too?

thk123 · 2018-04-03T09:54:08Z

src/goto-programs/replace_function_bodies.cpp

+        }
+        else if(!parameter.type().subtype().get_bool(ID_C_constant))
+        {
+          warning() << "warning: not havoccing non-const pointer parameter '"


Ah I see - this is why the tests are "wrong". I assume there is an issue? Probably worth ensuring this warning appears in the test and there is an appropriate comment on the issue to update the test.

This is all intended behaviour for now, I had asked around what people thought the right behaviour should be and it was "just skip structs with const members for now". The other behaviour is also possible, would that be your preference then?

On the face of it it seems more "correct" as I can easily write a method body for that method that violates that assert without wandering into undefined behaviour or even something particularly odd. That said, I'm not using this tool on a regular basis, it might be in the real world this is simply a more useful behaviour.

hannes-steffenhagen-diffblue · 2018-04-03T16:50:12Z

@thk123 I've now changed the behaviour so that structs, unions and arrays are traversed during havoccing instead of giving up when they contain constant elements.

hannes-steffenhagen-diffblue · 2018-04-05T10:36:08Z

There is some documentation about the feature in doc/cprover-manual.md. Unfortunately this has also lead to merge conflicts, which I will try to resolve now.

hannes-steffenhagen-diffblue · 2018-04-05T11:23:13Z

I have rebased the changes onto the newest develop. Apologies for any inconveniences.

thk123

Thanks for changes and docs. I would suggest if the (?!__) thing is so important, you may want to add a warning in the code if the supplied regex matches __CPROVER since most people won't read the manual...

thk123 · 2018-04-06T10:37:53Z

regression/goto-instrument/replace-function-body-union-with-const-member/test.desc

+^\[main.assertion.6\] assertion globalUnion.is_const == 10: FAILURE$
+^\[main.assertion.7\] assertion paramUnion.non_const == 20: FAILURE$
+^\[main.assertion.8\] assertion paramUnion.is_const == 20: FAILURE$
+^VERIFICATION FAILED$


Missing new line

thk123 · 2018-04-06T10:41:49Z

This is approaching the point where GH refuses to load this page due to too many comments. It might be wise to close this and open a new PR if there are still outstanding comments.

hannes-steffenhagen-diffblue · 2018-04-06T13:52:44Z

@thk123 I might just end up doing that. Technical issues aside, it's starting to get to the point of being difficult to follow along with a lot of the discussion no longer being relevant due to code changes

tautschnig · 2018-04-06T15:14:11Z

From my point of view this is very close to be ready to be merged (but others might disagree). I'd actually just suggest to squash the commit series into a few meaningful commits, re-review, approve, and be happy :-)

hannes-steffenhagen-diffblue · 2018-04-06T16:47:28Z

@tautschnig I believe this is in a good state now. Would you mind taking another look at this once CI passes?

tautschnig

I think there is further room for cleaning up the closely related options, but certainly this is a good piece of work to go in and further work can follow.

One wishlist request: please put a comment in the CHANGELOG file, this is a user-visible feature.

tautschnig · 2018-04-06T18:42:09Z

regression/goto-instrument/generate-function-body-union-with-const-member/test.desc

+^\[main.assertion.6\] assertion globalUnion.is_const == 10: FAILURE$
+^\[main.assertion.7\] assertion paramUnion.non_const == 20: FAILURE$
+^\[main.assertion.8\] assertion paramUnion.is_const == 20: FAILURE$
+^VERIFICATION FAILED$


Github says there's no newline here.

tautschnig · 2018-04-06T19:34:06Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1522,9 +1535,10 @@ void goto_instrument_parse_optionst::help()
    " --check-invariant function   instruments invariant checking function\n"
    " --remove-pointers            converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
    " --splice-call caller,callee  prepends a call to callee in the body of caller\n"  // NOLINT(*)
+    " --undefined-function-is-assume-false\n"


Could we mark this as deprecated (possibly be removing it from help output, but leaving it in the .h file)? Also: is it now implemented via the new options? (Just being lazy, I should be able to figure out once I've completely read the code.)

The effect can be replicated with --generate-function-body '.*' --generate-function-body-options assume-false

Yes indeed - but then we could get rid of the code implementing undefined_function_abort_path, couldn't we?

@hannes-steffenhagen-diffblue I'd leave it to you whether to include such changes in this PR or instead just create an issue and make someone else (such as myself...) fix it.

I've created #2070 to cover the additional cleanup and will merge this PR now.

tautschnig · 2018-04-06T19:49:27Z

src/goto-instrument/goto_instrument_parse_options.h

@@ -86,7 +88,9 @@ Author: Daniel Kroening, [email protected]
  "(undefined-function-is-assume-false)" \
  "(remove-function-body):"\
  "(splice-call):" \
-  OPT_REMOVE_CALLS_NO_BODY
+  OPT_REMOVE_CALLS_NO_BODY \
+  OPT_REPLACE_FUNCTION_BODY


I think this might not be worth renaming to OPT_GENERATE...?

hannes-steffenhagen-diffblue · 2018-04-09T10:59:23Z

@tautschnig I added a short reference to the new option in CHANGELOG under a new "5.9" section

chrisr-diffblue

Looks good - thanks for all the extra work and polishing on this PR.

polgreen · 2018-04-17T13:02:37Z

I know this PR has already been merged, but I have a question about the documentation:

" /// Replace the function body with one based on the implementation
/// This will work the same whether or not the function already has a body"

Does "implementation" have a specific meaning, I thought it just meant the actual function body? I'm not sure how you would replace the function body with one based on the function body if there is no function body, or, if there is a body, how the body that it replaces the body with is based on the original body?

ad62682 Merge pull request diffblue#2071 from thk123/refactor/split-string-unit-tests fc8ba88 Revert to aborting precondition for function inputs 3e2ab6f Merge pull request diffblue#2080 from diffblue/java-bytecode-dependency 6ff1eec cbmc: remove dependency on java_bytecode 0bff19b Merge pull request diffblue#2049 from karkhaz/kk-factor-goto-model-processing 79e3b25 Merge pull request diffblue#2084 from tautschnig/has_subtype-test cd45b0b Test has_subtype on recursive data types 85ac315 Merge pull request diffblue#2082 from thomasspriggs/default_dstring_hash 28c2e8b Merge pull request diffblue#2065 from tautschnig/be-constructor afa6023 Merge pull request diffblue#2061 from tautschnig/simplify-extractbits 014d151 Factor out getting & processing goto-model 06b3adc Merge pull request diffblue#2077 from peterschrammel/stable-tmp-var-names 0b3170d Stabilize clinit wrapper function type parameters 3cd8bf4 Temporary vars tests for goto-diff 9f0626c Prefix temporary var names with function id ca678aa More permissive regression tests regarding tmp var suffixes 47951ca Merge pull request diffblue#2079 from romainbrenguier/bugfix/has-subtype-recursion dd73b1a Specify default hash function of `dstringt` to STL. fe8e589 Avoid infinite recursion in has_subtype 00b9bf6 Merge pull request diffblue#2051 from svorenova/generics_tg2717 cd4bfc3 Merge pull request diffblue#2078 from romainbrenguier/bool-literal-in-while-loop 67ea889 Use bool literal in while loop d229ad9 Merge pull request diffblue#2056 from diffblue/fix-regression-cbmc-memcpy1 506faf0 Refactor a function for base existence 617d388 Utility functions for generic types c07e6ca Update generic specialization map when replacing pointers ed26d0a Merge pull request diffblue#2058 from peterschrammel/stable-disjuncts b663734 Simplify extractbits(concatenation(...)) b091560 Typing and refactoring of simplify_extractbits 49ad1bd Merge pull request diffblue#974 from tautschnig/fix-assert-encoding 16e9599 Merge pull request diffblue#2063 from tautschnig/has-subtype 950f58b Merge pull request diffblue#2060 from tautschnig/opt-local-map 4222a94 Regression tests for unstable instanceof and virtual method disjuncts b44589e Make disjuncts in instanceof removal independent of class loading 3afff86 Make disjuncts in virtual method removal independent of class loading a385d9b Allowed split_string to be used on whitespace if not also trying to strip fe4a642 Merge pull request diffblue#2062 from tautschnig/no-has-deref 145f474 Adding tests for empty string edge cases 07009d4 Refactored test to run all combinations 252c24c Migrate old string utils unit tests e87edbf Removing wrong elements from the make file b165c52 make test work on 32-bit Linux b804570 Merge pull request diffblue#2048 from JohnDumbell/improvement/adding_null_object_id 61f14d8 Merge pull request diffblue#1962 from owen-jones-diffblue/owen-jones-diffblue/simplify-replace-java-nondet fdee7e8 Merge pull request diffblue#2059 from tautschnig/generalise-test 4625cc5 Extend global has_subexpr to take a predicate as has_subtype does e9ebd59 has_subtype(type, pred, ns) to search for contained type matching pred 1f1f67f Merge pull request diffblue#1889 from hannes-steffenhagen-diffblue/develop-feature_generate_function_bodies 048c188 Add unit test for java_replace_nondet 0fe48c9 Make remove_java_nondet work before remove_returns bcc4dc4 Use byte_extract_exprt constructor a1814a3 Get rid of thin (and duplicate) has_dereference wrapper 4122a28 Test to demonstrate assert bug on alpine d44bfd3 Also simplify assert structure found on alpine linux c5cde18 Do not generate redundant if statements in assert expansions 4fb0603 Make is_skip publicly available and use constant argument 5832ffd Negative numbers should also pass the test 3c23b28 Consistently disable simplify_exprt::local_replace_map da63652 Merge pull request diffblue#2054 from romainbrenguier/bugfix/clear-equations d77f6a2 Merge pull request diffblue#1831 from NathanJPhillips/feature/class-annotations 60c8296 Clear string_refinement equations (not dependencies) 314ed53 Correcting the value of ID_null_object 751a882 Factor out default CBMC options to static method 6f24009 Can now test for an option being set in optionst 9a8d937 Add to_annotated_type and enable type_checked_cast for annotated_typet ca77b4e Add test for added annotations b06a27d Introduce abstract qualifierst base class e6fb3bf Pretty printing of java_class_typet e22b95b Fix spurious virtual function related keywords 3ac6d17 Add type_dynamic_cast and friends for java_class_typet ce1f4d2 Add annotations to java_class_typet, its methods and fields f84753d Merge pull request diffblue#2042 from hannes-steffenhagen-diffblue/add_deprecate_macro 7a38669 Merge pull request diffblue#2017 from NathanJPhillips/feature/overlay-classes 75a4aec Revert "the deprecation will need to wait until codebase is clean" 67735b5 Disable deprecation warnings by default 0764f77 Merge pull request diffblue#2036 from romainbrenguier/id_array_list 690b606 Merge pull request diffblue#2039 from peterschrammel/fix-duplicate-msg-json-ui bba17d9 the deprecation will need to wait until codebase is clean 822c757 Regression test for redundant JSON message output de0644d Only force end of previous message if there actually is one. 5a637bf Merge pull request diffblue#2037 from hannes-steffenhagen-diffblue/add_deprecate_macro bff456a Merge pull request diffblue#2040 from tautschnig/remove-swp 87ebe90 Remove vim temp file 228c019 Fix duplicate message output in json-ui 0a2c43e Add DEPRECATED to functions documented as \deprecated 47f4b35 interval_sparse_arrayt constructor from array-list 026c4ca Declare an array_list_exprt class 50a2696 Define ID_array_list 513b67a Merge pull request diffblue#2038 from romainbrenguier/bugfix/assign-at-malloc-site c207106 Test with array of strings 60183a3 Assign string at malloc site 116fffd Add DEPRECATED macro to mark deprecated functions and variables 7952f2c Add option to generate function body to goto-instrument 3d4183a Add ability to overlay classes with new definitions of existing methods dbc2f71 Improve code and error message in infer_opaque_type_fields 7c0ea4d Tidied up java_class_loader_limitt git-subtree-dir: cbmc git-subtree-split: ad62682

hannes-steffenhagen-diffblue added the do not merge label Feb 27, 2018

hannes-steffenhagen-diffblue requested review from chrisr-diffblue, martin-cs and peterschrammel as code owners February 27, 2018 17:10

hannes-steffenhagen-diffblue force-pushed the develop-feature_generate_function_bodies branch 3 times, most recently from 43613c1 to 9d874aa Compare February 28, 2018 16:13

hannes-steffenhagen-diffblue commented Mar 8, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the develop-feature_generate_function_bodies branch from 9d874aa to 1c9b407 Compare March 12, 2018 15:32

hannes-steffenhagen-diffblue removed the do not merge label Mar 12, 2018

hannes-steffenhagen-diffblue force-pushed the develop-feature_generate_function_bodies branch from 54ca23e to b80eea6 Compare March 12, 2018 15:58

hannes-steffenhagen-diffblue requested review from cesaro, mgudemann, smowton and thk123 as code owners March 12, 2018 15:58

hannes-steffenhagen-diffblue force-pushed the develop-feature_generate_function_bodies branch 2 times, most recently from 9efca43 to ea1f752 Compare March 12, 2018 16:42

thk123 reviewed Mar 15, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the develop-feature_generate_function_bodies branch from ea1f752 to ca0553a Compare March 16, 2018 14:41

hannes-steffenhagen-diffblue requested review from kroening and tautschnig as code owners March 16, 2018 14:41

thk123 reviewed Mar 19, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the develop-feature_generate_function_bodies branch from 0ae6a9f to 44fb0b1 Compare March 26, 2018 14:29

tautschnig reviewed Mar 29, 2018

View reviewed changes

thk123 reviewed Apr 3, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the develop-feature_generate_function_bodies branch 4 times, most recently from 177a60a to 38ee140 Compare April 4, 2018 13:35

hannes-steffenhagen-diffblue force-pushed the develop-feature_generate_function_bodies branch 2 times, most recently from e835e6b to 8958d37 Compare April 5, 2018 11:22

tautschnig assigned hannes-steffenhagen-diffblue Apr 5, 2018

thk123 approved these changes Apr 6, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the develop-feature_generate_function_bodies branch from 616cfd1 to 29d9882 Compare April 6, 2018 16:43

tautschnig approved these changes Apr 6, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the develop-feature_generate_function_bodies branch from 29d9882 to ebfaf5a Compare April 9, 2018 10:56

Add option to generate function body to goto-instrument

7952f2c

hannes-steffenhagen-diffblue force-pushed the develop-feature_generate_function_bodies branch from ebfaf5a to 7952f2c Compare April 9, 2018 11:40

chrisr-diffblue approved these changes Apr 11, 2018

View reviewed changes

chrisr-diffblue mentioned this pull request Apr 16, 2018

Cleanup 'undefined-function' options to use 'generate-function-body' #2070

Open

chrisr-diffblue merged commit 1f1f67f into diffblue:develop Apr 16, 2018


		Module: Replace bodies of goto functions

		Author: DiffBlue Limited. All rights reserved.


		Module: Replace bodies of goto functions

		Author: DiffBlue Limited.


		Module: Replace bodies of goto functions

		Author: DiffBlue Ltd.

		@@ -0,0 +1,410 @@
		/*******************************************************************\

Add option to generate function body to goto-instrument #1889

Add option to generate function body to goto-instrument #1889

Conversation

hannes-steffenhagen-diffblue commented Feb 27, 2018 • edited Loading

tautschnig commented Feb 27, 2018

hannes-steffenhagen-diffblue commented Feb 28, 2018 • edited Loading

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

martin-cs commented Mar 8, 2018

martin-cs commented Mar 8, 2018

martin-cs commented Mar 8, 2018

hannes-steffenhagen-diffblue commented Mar 13, 2018

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue Mar 15, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue commented Mar 16, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue commented Mar 29, 2018

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue commented Apr 3, 2018

hannes-steffenhagen-diffblue commented Apr 5, 2018

hannes-steffenhagen-diffblue commented Apr 5, 2018

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 commented Apr 6, 2018

hannes-steffenhagen-diffblue commented Feb 27, 2018 •

edited

Loading

hannes-steffenhagen-diffblue commented Feb 28, 2018 •

edited

Loading

hannes-steffenhagen-diffblue Mar 15, 2018 •

edited

Loading

hannes-steffenhagen-diffblue Apr 9, 2018 •

edited

Loading